COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		Mathematical logicians, beginning with Kurt Goedel (192x), often
C00005 ENDMK
C⊗;
	Mathematical logicians, beginning with Kurt Goedel (192x), often
represent symbolic expressions by so-called Goedel numbers.  Symbolic
computations such as those involved in checking a proof in number
theory can then be replaced by numerical computations involving
the Goedel numbers of the sentences involved in the proof.  Sentences
about the existence of proofs of sentences can then be replaced
by sentences of number theory
about the existence of the Goedel numbers of the proofs.  This enabled
Goedel to find a sentence of number theory that in essence asserts its
own unprovability.  

	There are many systems of Goedel numbering, i.e. of assigning
numbers to expressions, but in order to be metamathematically useful,
they must all have the following properties.  First, the structure
of the expression must be determinable from its Goedel number, and
second the elementary processes of symbolic computation must correspond
to simple numerical computations.  Thus we may have

	%2gn(<the n th variable>) = 2↑n%1,

	%2gn(<the n th natural number>) = 3↑n%1,

and

	%2gn("ab + c") = 5↑gn("ab")7↑gn("c")%1.

Such a rule permits identifying the Goedel number of a variable by
the fact that only they are divisible by 2.  The Goedel number
of a natural number is a power of three, and the number itself can
be obtained by computing the exponent.  Likewise sums can be
identified and the summands extracted by simple numerical computation.